Inference at * 1 1 1 
Iof proof for Lemma list extensionality:

.....subterm..... T:t1:n

1. T : Type
2. T List
3. u : T
4. v : T List
5. b:(T List). (||v|| = ||b||)  (i:. (i < ||v||)  (v[i] = b[i]))  (v = b)
6. T List
7. u1 : T
8. v1 : T List
9. (||[u / v]|| = ||v1||)  (i:. (i < ||[u / v]||)  ([u / v][i] = v1[i]))  ([u / v] = v1)
10. ||v||+1 = ||v1||+1
11. i:. (i < (||v||+1))  ([u / v][i] = [u1 / v1][i])
  u = u1 

latex

 by ((((((InstHyp [0] (-1)) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 
C3:n)) (first_tok SupInf:t) inil_term)))) 
CollapseTHEN (Reduce (-1)))) 
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions	t  T, ff, tt, i <z j, b, i z j, if b then t else f fi , Y, nth_tl(n;as), hd(l), l[i], P  Q, x:A. B(x)
Lemmas	non neg length